(declare-fun __CONGRUENCE_25 () Int)
(declare-fun __INITIAL_LOCATION () Int)
(declare-fun |main::i@3| () Int)
(declare-fun |main::j@4| () Int)
(declare-fun |main::i@4| () Int)
(declare-fun __CONGRUENCE_26 () Int)
(declare-fun |main::j@3| () Int)
(assert (and (= __INITIAL_LOCATION 2) (>= |main::j@3| |main::i@3|) (= |main::i@4| (+ 2 |main::i@3|)) (= |main::j@4| (+ (- 1) |main::j@3|))))
(assert (and (= __INITIAL_LOCATION 2) (= |main::i@3| (+ 1 (* 2 __CONGRUENCE_25))) (= |main::j@3| (+ 0 (* 2 __CONGRUENCE_26))) (<= (+ (* (- 1) |main::j@3|) (* |main::i@3| (- 2))) (- 12)) (<= (+ (* |main::j@3| 2) (* (- 1) |main::i@3|)) 19) (<= (+ (* |main::j@3| 2) |main::i@3|) 21) (<= (+ |main::j@3| (* (- 1) |main::i@3|)) 9) (<= (+ |main::j@3| (* |main::i@3| (- 2))) 8) (<= (+ (* |main::j@3| (- 2)) (* (- 1) |main::i@3|)) (- 21)) (<= |main::i@3| 1) (<= (+ (* (- 1) |main::j@3|) (* |main::i@3| 2)) (- 8)) (<= (+ |main::j@3| (* |main::i@3| 2)) 12) (<= (* (- 1) |main::i@3|) (- 1)) (<= (+ |main::i@3| (* (- 1) |main::j@3|)) (- 9)) (<= |main::j@3| 10) (<= (+ (* (- 1) |main::j@3|) (* (- 1) |main::i@3|)) (- 11)) (<= (+ |main::j@3| |main::i@3|) 11) (<= (* (- 1) |main::j@3|) (- 10)) (<= (+ (* |main::j@3| (- 2)) |main::i@3|) (- 19))))
(assert (> (+ |main::j@4| (* |main::i@4| (- 2))) 8))
(check-sat)
